﻿using System.Collections;
using System.Collections.Generic;

namespace Tautologie
{
    class TruthTable
    {
        List<BitArray> Table;
        List<string> Labels; // i.e. "Kpq", which means conjunction of p and q
                                   //"AKpqr, which means disjunction of p and q conjunction and r

        public TruthTable(int Sentences)
        {
            Table = new List<BitArray>();
            Labels = new List<string>();
            switch (Sentences)
            {
                case 1:
                    Table.Add(new BitArray(new bool[] { false, true }));
                    Labels.Add("p");
                    break;
                case 2:
                    Table.Add(new BitArray(new bool[] { false, false, true, true }));
                    Table.Add(new BitArray(new bool[] { false, true, false, true }));
                    Labels.Add("p");
                    Labels.Add("q");
                    break;
                case 3:
                    Table.Add(new BitArray(new bool[] { false, false, false, false, true, true, true, true }));
                    Table.Add(new BitArray(new bool[] { false, false, true, true, false, false, true, true }));
                    Table.Add(new BitArray(new bool[] { false, true, false, true, false, true, false, true }));
                    Labels.Add("p");
                    Labels.Add("q");
                    Labels.Add("r");
                    break;
            }
        }

        public int AddNegation(int Column)
        {
            BitArray temp = (BitArray)Table[Column].Clone(); //creates new copy in order not to modify anything
            Table.Add(temp.Not()); //adds new BitArray object to list
            return Table.Count - 1; //returns a new expression's index
        }

        public int AddConjuction(int Column1, int Column2)
        {
            BitArray temp = (BitArray)Table[Column1].Clone();
            Table.Add(temp.And(Table[Column2]));
            return Table.Count - 1;
        }

        public int AddDisjuncion(int Column1, int Column2)
        {
            BitArray temp = (BitArray)Table[Column1].Clone();
            Table.Add(temp.Or(Table[Column2]));
            return Table.Count - 1;
        }

        public int AddImplication(int Column1, int Column2)
        {
            BitArray temp = (BitArray)Table[Column1].Clone();
            Table.Add(temp.Imp(Table[Column2]));
            return Table.Count - 1;
        }

        public bool IsSentence(char c)
        {
            //Checks if argument is defined logical sentence (N, C, A or K)
            //returns false when user typed i.e. "F"
            if (Labels.Contains(c.ToString())) return true;
            else return false;
        }

        public int FindIndex(string a)
        {
            //Searches and returns a given expression's index
            return Labels.IndexOf(a);
        }

        public override string ToString()
        {
            string Result = "";
            for (int i = 0; i < Table[0].Length; i++)
            {
                for (int j = 0; j < Table.Count; j++)
                {
                    if (Table[j][i] == true) Result += 1 + " ";
                    else Result += 0 + " ";
                }
                Result += "\n";
            }
            return Result;
        }

        public string[] ReturnLabels()
        {
            return Labels.ToArray();
        }

        public void AddLabel(string label)
        {
            //Add label to List<string> Labels
            Labels.Add(label);
        }

        public int[] CheckIfTautology()
        {
            //returns indexes of all tautologies, if there is no tautology, returns empty array
            List<int> result = new List<int>();
            for (int i = 0; i < Table.Count; i++)
            {
                if (Table[i].IfAllElementsAreTrue())
                    result.Add(i);
            }
            return result.ToArray();
        }
    }
}
